Nuprl Lemma : assert_of_band 9,38

p,q:. ((p  q))  ((p (q)) 
latex


ProofTree


Definitionst  T, x:AB(x), , P  Q, P  Q, True, ff, if b then t else f fi , tt, P  Q, p  q, b, P  Q, False, Unit, ,
Lemmasbool wf, false wf, true wf

origin